Skip to content

Else simplification pass#214

Open
DCupello1 wants to merge 7 commits intoletintro-passfrom
else-simp-pass
Open

Else simplification pass#214
DCupello1 wants to merge 7 commits intoletintro-passfrom
else-simp-pass

Conversation

@DCupello1
Copy link

@DCupello1 DCupello1 commented Jan 15, 2026 •
edited
Loading

This pass is towards a better representation of otherwise when the only concern are boolean premises. This simply takes the original premises of the generated relations and negates them.

Example:

relation Step_pure: admininstr* ~> admininstr*
rule Step_pure/br_if-true:
  (CONST I32 c) (BR_IF l)  ~>  (BR l)
  -- if c =/= 0

rule Step_pure/br_if-false:
  (CONST I32 c) (BR_IF l)  ~>  eps
  -- otherwise

From else pass (omitting wf premises):

relation `Step_pure_before_br_if-false`: `%`(admininstr*)
  rule `br_if-true_0`{c : val_, l : labelidx}:
    `%`([CONST_admininstr(I32_valtype, c) BR_IF_admininstr(l)])
    -- if (!($proj_val__0(c))!`%`_uN.0 =/= 0)
    
relation Step_pure: `%~>%`(admininstr*, admininstr*)
  rule `br_if-true`{c : val_, l : labelidx}:
    `%~>%`([CONST_admininstr(I32_valtype, c) BR_IF_admininstr(l)], [BR_admininstr(l)])
    -- if (!($proj_val__0(c))!`%`_uN.0 =/= 0)

  rule `br_if-false`{c : val_, l : labelidx}:
    `%~>%`([CONST_admininstr(I32_valtype, c) BR_IF_admininstr(l)], [])
    -- ~ `Step_pure_before_br_if-false`: `%`([CONST_admininstr(I32_valtype, c) BR_IF_admininstr(l)])

From else simplification pass:

relation Step_pure: `%~>%`(admininstr*, admininstr*)
  rule `br_if-true`{c : val_, l : labelidx}:
    `%~>%`([CONST_admininstr(I32_valtype, c) BR_IF_admininstr(l)], [BR_admininstr(l)])
    -- if (!($proj_val__0(c))!`%`_uN.0 =/= 0)

  rule `br_if-false`{c : val_, l : labelidx}:
    `%~>%`([CONST_admininstr(I32_valtype, c) BR_IF_admininstr(l)], [])
    -- if (!($proj_val__0(c))!`%`_uN.0 = 0)

Based off of #213 , currently a draft until we iron out the details for this pass. (And modify tests)

@DCupello1 DCupello1 changed the base branch from main to letintro-pass January 15, 2026 14:03
@DCupello1 DCupello1 marked this pull request as ready for review February 24, 2026 12:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@DCupello1